(TML)
newtypes [ ``list = . + clist`` ;
           ``clist = atom # list`` ] ;;

map newconstant
[ `NIL`      , ":list"
; `NULL`     , ":list->tr"
; `HEAD`     , ":list->atom"
; `TAIL`     , ":list->list"
; `CONS`     , ":atom->list->list"
; `APPEND`   , ":list->list->list"
; `LISTFUN`  , ":(list->list) -> (list->list)"
] ;;

let defNIL = ASSUME "NIL == INL()"
;; let defNULL = ASSUME "NULL == ISL"
;; let defHEAD = ASSUME "HEAD == \L. FST(OUTR L)"
;; let defTAIL = ASSUME "TAIL == \L. SND(OUTR L)"
;; let defCONS = ASSUME "CONS == \A L. INR(A,L)"
;; let defAPPEND = ASSUME "APPEND == FIX \F. \L L' .
                           NULL L => L' | CONS(HEAD L)(F(TAIL L)L')"
;;  let defLISTFUN = ASSUME "LISTFUN ==
                     \G.\L. NULL L => NIL | CONS(HEAD L)(G(TAIL L))"
;;

let LISTAX = ASSUME "!L. FIX LISTFUN L == L" ;;